Search Results

Documents authored by Exibard, Léo

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.122
A Generic Solution to Register-Bounded Synthesis with an Application to Discrete Orders

Authors: Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata is undecidable in general. However, its register-bounded variant, where additionally a bound on the number of registers in a sought transducer is given, is known to be decidable for universal register automata which can compare data for equality, i.e., for data domain (ℕ, =). This paper extends the decidability border to the domain (ℕ, <) of natural numbers with linear order. Our solution is generic: we define a sufficient condition on data domains (regular approximability) for decidability of register-bounded synthesis. The condition is satisfied by natural data domains like (ℕ, <). It allows one to use simple language-theoretic arguments and avoid technical game-theoretic reasoning. Further, by defining a generic notion of reducibility between data domains, we show the decidability of synthesis in the domain (ℕ^d, <^d) of tuples of numbers equipped with the component-wise partial order and in the domain (Σ^*,≺) of finite strings with the prefix relation.
Cite as

Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov. A Generic Solution to Register-Bounded Synthesis with an Application to Discrete Orders. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 122:1-122:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{exibard_et_al:LIPIcs.ICALP.2022.122,
  author =	{Exibard, L\'{e}o and Filiot, Emmanuel and Khalimov, Ayrat},
  title =	{{A Generic Solution to Register-Bounded Synthesis with an Application to Discrete Orders}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{122:1--122:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.122},
  URN =		{urn:nbn:de:0030-drops-164634},
  doi =		{10.4230/LIPIcs.ICALP.2022.122},
  annote =	{Keywords: Synthesis, Register Automata, Transducers, Ordered Data Domains}
}
Document
DOI: 10.4230/LIPIcs.STACS.2021.28
Church Synthesis on Register Automata over Linearly Ordered Data Domains

Authors: Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov

Published in: LIPIcs, Volume 187, 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)

Abstract
Register automata are finite automata equipped with a finite set of registers in which they can store data, i.e. elements from an unbounded or infinite alphabet. They provide a simple formalism to specify the behaviour of reactive systems operating over data ω-words. We study the synthesis problem for specifications given as register automata over a linearly ordered data domain (e.g. (ℕ, ≤) or (ℚ, ≤)), which allow for comparison of data with regards to the linear order. To that end, we extend the classical Church synthesis game to infinite alphabets: two players, Adam and Eve, alternately play some data, and Eve wins whenever their interaction complies with the specification, which is a language of ω-words over ordered data. Such games are however undecidable, even when the specification is recognised by a deterministic register automaton. This is in contrast with the equality case, where the problem is only undecidable for nondeterministic and universal specifications. Thus, we study one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show they are determined, and deciding the existence of a winning strategy is in ExpTime, both for ℚ and ℕ. This follows from a study of constraint sequences, which abstract the behaviour of register automata, and allow us to reduce Church games to ω-regular games. Lastly, we apply these results to the transducer synthesis problem for input-driven register automata, where each output data is restricted to be the content of some register, and show that if there exists an implementation, then there exists one which is a register transducer.
Cite as

Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov. Church Synthesis on Register Automata over Linearly Ordered Data Domains. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 187, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{exibard_et_al:LIPIcs.STACS.2021.28,
  author =	{Exibard, L\'{e}o and Filiot, Emmanuel and Khalimov, Ayrat},
  title =	{{Church Synthesis on Register Automata over Linearly Ordered Data Domains}},
  booktitle =	{38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-180-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{187},
  editor =	{Bl\"{a}ser, Markus and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2021.28},
  URN =		{urn:nbn:de:0030-drops-136735},
  doi =		{10.4230/LIPIcs.STACS.2021.28},
  annote =	{Keywords: Synthesis, Church Game, Register Automata, Transducers, Ordered Data Words}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.24
Synthesis of Data Word Transducers

Authors: Léo Exibard, Emmanuel Filiot, and Pierre-Alain Reynier

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals (omega-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite. In this paper, we consider data omega-words instead, i.e., words over an infinite alphabet. In this context, we study specifications and implementations respectively given as automata and transducers extended with a finite set of registers. We consider different instances, depending on whether the specification is nondeterministic, universal or deterministic, and depending on whether the number of registers of the implementation is given or not. In the unbounded setting, we show undecidability for both universal and non-deterministic specifications, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but can be recovered by disallowing tests over input data. The generic technique we use to show the latter result allows us to reprove some known result, namely decidability of bounded synthesis for universal specifications.
Cite as

Léo Exibard, Emmanuel Filiot, and Pierre-Alain Reynier. Synthesis of Data Word Transducers. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{exibard_et_al:LIPIcs.CONCUR.2019.24,
  author =	{Exibard, L\'{e}o and Filiot, Emmanuel and Reynier, Pierre-Alain},
  title =	{{Synthesis of Data Word Transducers}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.24},
  URN =		{urn:nbn:de:0030-drops-109269},
  doi =		{10.4230/LIPIcs.CONCUR.2019.24},
  annote =	{Keywords: Register Automata, Synthesis, Data words, Transducers}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.46
The Complexity of Transducer Synthesis from Multi-Sequential Specifications

Authors: Léo Exibard, Emmanuel Filiot, and Ismaël Jecker

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
The transducer synthesis problem on finite words asks, given a specification S subseteq I x O, where I and O are sets of finite words, whether there exists an implementation f: I - > O which (1) fulfils the specification, i.e., (i,f(i))in S for all i in I, and (2) can be defined by some input-deterministic (aka sequential) transducer T_f. If such an implementation f exists, the procedure should also output T_f. The realisability problem is the corresponding decision problem. For specifications given by synchronous transducers (which read and write alternately one symbol), this is the finite variant of the classical synthesis problem on omega-words, solved by Büchi and Landweber in 1969, and the realisability problem is known to be ExpTime-c in both finite and omega-word settings. For specifications given by asynchronous transducers (which can write a batch of symbols, or none, in a single step), the realisability problem is known to be undecidable. We consider here the class of multi-sequential specifications, defined as finite unions of sequential transducers over possibly incomparable domains. We provide optimal decision procedures for the realisability problem in both the synchronous and asynchronous setting, showing that it is PSpace-c. Moreover, whenever the specification is realisable, we expose the construction of a sequential transducer that realises it and has a size that is doubly exponential, which we prove to be optimal.
Cite as

Léo Exibard, Emmanuel Filiot, and Ismaël Jecker. The Complexity of Transducer Synthesis from Multi-Sequential Specifications. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{exibard_et_al:LIPIcs.MFCS.2018.46,
  author =	{Exibard, L\'{e}o and Filiot, Emmanuel and Jecker, Isma\"{e}l},
  title =	{{The Complexity of Transducer Synthesis from Multi-Sequential Specifications}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{46:1--46:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.46},
  URN =		{urn:nbn:de:0030-drops-96286},
  doi =		{10.4230/LIPIcs.MFCS.2018.46},
  annote =	{Keywords: Transducers, Multi-Sequentiality, Synthesis}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact